其他
Move硬核研究系列 | 智能合约的重要变革,如何使用Move Prover?
#安装
git clone [https://github.com/move-language/move.git](https://github.com/move-language/move.git)
cd move && ./scripts/dev_setup.sh -ypt
move prove -t TEST_NAME
#应用场景
1 权限控制
在规范层面上强制执行明确的访问控制策略可以有效防止权限滥用。
例如,在std::offer中,我们可以看到,当接收者不在白名单中,该函数会被终止。
spec redeem {
...
aborts_if !is_allowed_recipient<Offered>(offer_address, signer::address_of(account));
...
}
struct Account has key {
balance: u64
}
const MAX_BALANCE: u64 = 1000;
fun deposit(target: address, amount: u64) acquires Account {
let account = borrow_global_mut<Account>(target);
let new_balance = account.balance + amount;
assert!(new_balance <= MAX_BALANCE, 0);
account.balance = new_balance;
}
invariant forall a: address where exists<Account>(a):
balance(a) <= MAX_BALANCE;
public fun swap<X, Y, Curve>(
x_in: Coin<X>,
y_in: Coin<Y>,
): (Coin<X>, Coin<Y>) acquires Pool {
...
let x_reserve_size = coin::value(&pool.coin_x_reserve);
let y_reserve_size = coin::value(&pool.coin_y_reserve);
// Deposit new coins to Pool.
coin::merge(&mut pool.coin_x_reserve, x_in);
coin::merge(&mut pool.coin_y_reserve, y_in);
spec {
coin::value(&pool.coin_x_reserve) > x_reserve_size || coin::value(&pool.coin_y_reserve) > y_reserve_size;
};
...
}